\begin{tabbing}
state ${\it ds}$
\\[0ex]$k$:$A$ sends [${\it tg}$, $e$.$f$($e$):$B$] on $l$
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(($\forall$$e$:E. (kind($e$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $B$))\+
\\[0ex]\& ($\forall$$x$:Id. vartype(source($l$);$x$) $\subseteq$r ${\it ds}$($x$)?Top)
\\[0ex]\& ($\forall$$e$:E. (kind($e$) = $k$) $\Rightarrow$ (loc($e$) = source($l$)) $\Rightarrow$ (valtype($e$) $\subseteq$r $A$)))
\\[0ex]c$\wedge$ \=(\=$\forall$$e$@source($l$).\+\+
\\[0ex](kind($e$) = $k$) $\Rightarrow$ ($\uparrow$isl($f$($e$))) $\Rightarrow$ ($\exists$${\it e'}$:E. (kind(${\it e'}$) = rcv($l$,${\it tg}$) \& sender(${\it e'}$) = $e$))
\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex](kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=((kind(sender(${\it e'}$)) = $k$)\+
\\[0ex]c$\wedge$ ($\uparrow$isl($f$(sender(${\it e'}$))))
\\[0ex]c$\wedge$ (val(${\it e'}$) = outl($f$(sender(${\it e'}$))))))
\-\-\\[0ex]\& (\=$\forall$${\it e'}$:E.\+
\\[0ex](kind(${\it e'}$) = rcv($l$,${\it tg}$))
\\[0ex]$\Rightarrow$ \=($\forall$${\it e''}$:E.\+
\\[0ex](kind(${\it e''}$) = rcv($l$,${\it tg}$)) $\Rightarrow$ (sender(${\it e''}$) = sender(${\it e'}$)) $\Rightarrow$ (${\it e''}$ = ${\it e'}$))))
\-\-\-\-
\end{tabbing}